Nuprl Lemma : es-causl-p-locl-test
11,40
postcript
pdf
es
:ES,
p
:(E
(E + Top)).
causal-predecessor(
es
;
p
)
(
e
,
e'
,
a
,
b
:E.
a
c
e
e
p
e'
e'
p
<
b
(
a
<
b
))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
,
x
{FDLNOr12445}
Lemmas
event
system
wf
,
top
wf
,
causal-predecessor
wf
,
es-E
wf
,
es-causle
wf
,
es-p-le
wf
,
es-p-locl
wf
,
es-causl
transitivity1
,
es-causle
transitivity
,
es-causle
weakening
p-le
,
es-causl
weakening
p-locl
origin
es:ES, p:(E
(E + Top)).
(e, e', a, b:E. a c
e e p e' e' p< b (a < b)) es:ES, p:(E(E + Top)).
(e, e', a, b:E. a c e e p e' e' p< b (a < b)) 
T Qx:A. B(x)